'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: {f(s(x), y, y) -> f(y, x, s(x))} Details: We have computed the following set of weak (innermost) dependency pairs: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} The usable rules are: {} The estimated dependency graph contains the following edges: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} ==> {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} We consider the following path(s): 1) {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} The usable rules for this path are empty. We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Details: 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Details: The problem was solved by processor 'combine': 'combine' --------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Details: 'sequentially if-then-else, sequentially' ----------------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Weak Rules: {} Details: 'if Check whether the TRS is strict trs contains single rule then fastest else fastest' --------------------------------------------------------------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Weak Rules: {} Details: a) We first check the conditional [Success]: We are considering a strict trs contains single rule TRS. b) We continue with the then-branch: The problem was solved by processor 'fastest of 'Matrix Interpretation', 'Matrix Interpretation', 'Matrix Interpretation'': 'fastest of 'Matrix Interpretation', 'Matrix Interpretation', 'Matrix Interpretation'' -------------------------------------------------------------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Weak Rules: {} Details: The problem was solved by processor 'Matrix Interpretation': 'Matrix Interpretation' ----------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: {f^#(s(x), y, y) -> c_0(f^#(y, x, s(x)))} Weak Rules: {} Details: Interpretation Functions: f(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0] s(x1) = [1] x1 + [6] f^#(x1, x2, x3) = [6] x1 + [4] x2 + [2] x3 + [1] c_0(x1) = [1] x1 + [0]